Symbolic execution is a popular, automatic approach for testing software, generating test cases, and finding bugs. Symbolic execution was discovered in 1975, with the volume of academic research and commercial systems exploding in the last decade. The online bibliography at http://sites.google.com/site/symexbib lists over 150 papers on symbolic execution techniques and applications, and published surveys exist. Notable examples include “SAGE” and “KLEE.” SAGE was responsible for finding one third of all bugs discovered by file fuzzing during the development of Windows 7. KLEE was the first tool to show that symbolic execution can generate test cases that achieve high coverage on real programs by demonstrating it on the UNIX utilities. There is a multitude of symbolic execution systems. For more details, various surveys may be consulted.
Over the past decade, numerous symbolic execution tools have appeared—both in academia and industry—showing the effectiveness of the technique in finding crashing inputs, generating test cases with high coverage, exposing software vulnerabilities, and generating exploits.
Symbolic execution can be attractive, because it systematically explores the software code (e.g., program) and produces real inputs. Symbolic execution operates by automatically translating a software code fragment (e.g., a program fragment) into a formula (e.g., a symbolic expression) in logic. The logical formula is then solved to determine inputs that have a desired property (e.g., executing the desired execution paths or violating safety). Such inputs satisfy the formula with respect to that desired property.
There are two main approaches for generating formulas. First, dynamic symbolic exploration (DSE) explores software code (e.g., programs) and generates formulas on a per-path basis. Second, static symbolic execution (SSE) translates executable statements (not execution paths) into formulas, where the formulas represent the desired property over any path within the selected statements.
Merging execution paths was pioneered by Koelbl et al. in SSE. Concurrently and independently, Xie et al. developed Saturn, a verification tool capable of encoding multiple paths before converting the problem to a Boolean Satisfiability Problem (SAT). Hansen et al. followed an approach similar to Koelbl et al. at the binary level. Babic improved the static algorithm of Hansen et al. to produce smaller and faster approaches to solve formulas by leveraging Gated Single Assignment (GSA) and maximally-shared graphs (similar to hash-consing).
The efficiency of above static algorithms typically stems from various types of if-conversion, a technique for converting code with branches into predicated straightline statements. The technique is also known as φ-folding, a compiler optimization technique that collapses simple diamond-shaped structures in the control flow graph (CFG). Collingbourne et al. used φ-folding to verify semantic equivalence of single instruction, multiple data (SIMD) instructions.
Boonstoppel et al. proposed RWSet, a state pruning technique identifying redundant states based on similarity of their live variables. If live variables of a state are equivalent to a previously explored path, RWSet will stop exploring the states, as it will not offer additional coverage.
Godefroid et al. introduced function summaries to test code compositionally. The main idea is to record the output of an analyzed function, and to reuse it if it is called again with similar arguments. This work was later expanded to generate such summaries on demand [40].